perm filename DEMO[P,JRA] blob
sn#525177 filedate 1980-07-27 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00009 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 as you can see "" is the comment delimiter
C00018 00003 stuff needed all over
C00023 00004 (def is_fundef ()
C00054 00005 (def readspec ()
C00057 00006 (def repclauses ()
C00071 00007 (def translate (name target)
C00082 00008 top level
C00091 00009 stuff needed for lisp to run generated programs
C00127 ENDMK
C⊗;
;as you can see ";" is the comment delimiter
;this is the working version, precond check has been moved inside function
;definition, and functions return substitutions
(putprop 'def (get 'defun 'fsubr) 'fsubr)
;primitive function and type definitions
;for LISP
(PROG2
(putprop 'lisp '( (def integer fexpr (l)
(cond ((eq (length l) 1)
(cond ((fixp (first l)) ())
(t 'undef)))
((is-constant (second l))
(cond ((fixp (first l))
(cond ((or (eq (second l) 'true)
(eq (second l) t)) () )
(t 'undef)))
((or (eq (second l) 'undef)
(eq (second l) 'false)) ())
(t 'undef)))
(t (list (cons (second l)
(cond ((fixp (first l)) t)
(t 'false)))))))
(def real fexpr (l)
(cond ((eq (length l) 1)
(cond ((floatp (first l)) ())
(t 'undef)))
((is-constant (second l))
(cond ((floatp (first l))
(cond ((or (eq (second l) 'true)
(eq (second l) t)) () )
(t 'undef)))
((or (eq (second l) 'undef)
(eq (second l) 'false)) ())
(t 'undef)))
(t (list (cons (second l)
(cond ((floatp (first l)) t)
(t 'false)))))))
(def boolean fexpr (l)
(cond ((eq (length l) 1)
(cond ((or (eq (first l) t)
(eq (first l) 'true)
(eq (first l) 'undef)
(eq (first l) 'false)) ())
(t 'undef)))
((is-constant (second l))
(cond ((or (eq (first l) t)
(eq (first l) 'true)
(eq (first l) 'undef)
(eq (first l) 'false))
(cond ((or (eq (second l) 'true)
(eq (second l) t)) () )
(t 'undef)))
((or (eq (second l) 'undef)
(eq (second l) 'false)) ())
(t 'undef)))
(t (list (cons (second l)
(cond
((or (eq (first l) t)
(eq (first l) 'true)
(eq (first l) 'undef)
(eq (first l) 'false)) t)
(t 'false)))))))
(def ≤ fexpr (l)
(cond ((eq (length l) 2)
(cond ((or (old< (first l) (second l))
(old= (first l) (second l))) ())
(t 'undef)))
((is-constant (third l))
(cond ((or (old< (first l) (second l))
(old= (first l) (second l)))
(cond ((or (eq (third l) t)
(eq (third l) 'true)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef))())
(t 'undef)))
(t (list (cons (third l)
(cond ((or (old< (first l) (second l))
(old= (first l) (second l)))
t)
(t 'false)))))))
(def ≥ fexpr (l)
(cond ((eq (length l) 2)
(cond ((or (old> (first l) (second l))
(old= (first l) (second l))) ())
(t 'undef)))
((is-constant (third l))
(cond ((or (old> (first l) (second l))
(old= (first l) (second l)))
(cond ((or (eq (third l) t)
(eq (third l) 'true)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef))())
(t 'undef)))
(t (list (cons (third l)
(cond ((or (old> (first l) (second l))
(old= (first l) (second l)))
t)
(t 'false)))))))
(def ≠ fexpr (l)
(cond ((eq (length l) 2)
(cond ((old= (first l) (second l)) 'undef)
(t ())))
((is-constant (third l))
(cond ((old= (first l) (second l))
(cond ((or (eq (third l) 'undef)
(eq (third l) 'false)) ())
(t 'undef)))
((or (eq (third l) 'true)
(eq (third l) t))())
(t 'undef)))
(t (list (cons (third l)
(cond ((old= (first l) (second l))
'false)
(t t)))))))
(putprop 'old< (get '< 'subr) 'subr)
(putprop 'old> (get '> 'subr) 'subr)
(putprop 'old= (get '= 'subr) 'subr)
(def < fexpr (l)
(cond ((eq (length l) 2)
(cond ((old< (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((old< (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((old< (first l) (second l)) t)
(t 'false)))))))
(def ∨ fexpr (l)
(cond ((eq (length l) 2)
(cond ((or (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((or (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'undef)
(eq (third l) 'false)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((or (first l) (second l)) t)
(t 'false)))))))
(def ∧ fexpr (l)
(cond ((eq (length l) 2)
(cond ((and (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((and (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'undef)
(eq (third l) 'false)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((and (first l) (second l)) t)
(t 'false)))))))
(def > fexpr (l)
(cond ((eq (length l) 2)
(cond ((old> (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((old> (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((old> (first l) (second l)) t)
(t 'false)))))))
(def = fexpr (l)
(cond ((eq (length l) 2)
(cond ((old= (first l) (second l)) ())
(t 'undef)))
((is-constant (third l))
(cond ((old= (first l) (second l))
(cond ((or (eq (third l) 'true)
(eq (third l) t)) ())
(t 'undef)))
((or (eq (third l) 'false)
(eq (third l) 'undef)) ())
(t 'undef)))
(t (list (cons (third l)
(cond ((old= (first l) (second l)) t)
(t 'false)))))))
; (def + (x y) (+ x y))
; (def - (x y) (- x y))
; (def * (x y) (* x y))
; (def // (x y) (// x y))
(def r+ (x y) (+$ x y))
(def r- (x y) (-$ x y))
(def r* (x y) (*$ x y))
(def r// (x y) (//$ x y))
;stuff for adding strings which are represented as a list of 2 elements,
; the first is the atom STRING, the second is a list of the characters in the
; string.
(def readstring ()
(prog (temp hdr)
(setq temp (cons (readch) () ))
(setq hdr (cons temp temp))
(return (do ((nxtchar (readch) (readch)))
((and (eq nxtchar '")
(not (eq (tyipeek) 42)))
(list 'string (car hdr)))
(cond ((eq nxtchar '")(readch)))
(setq temp (cons nxtchar () ))
(rplacd (cdr hdr) temp)
(rplacd hdr temp)))))
(def string fexpr (l) (cons 'string l))
(setsyntax '" 'macro 'readstring)
(putprop 'prt (get 'print 'subr) 'subr)
(def print (x)
(cond ((eq x nil) (prt '/( ) (princ '/) ))
((or (atom x) (not (eq (first x) 'string)))
(prt x))
(t (prt (maknam (second x))))))
(def is-string fexpr (x)
(cond ((eq (length x) 1)
((lambda (y)
(cond
((and (not (atom y))
(eq (first y) 'string)
(null (rest (rest y)))) ())
(t 'undef)))
(eval (first x))))
(t ((lambda (y1 y2)
(cond
((and (not (atom y1))
(eq (first y1) 'string)
(null (rest (rest y1))))
(cond ((or (eq y2 'true)
(eq y2 t)) ())
((or (eq y2 'false)
(eq y2 'undef)) 'undef)
(t (list (cons y2 t)))))
((or (eq y2 'false)
(eq y2 'undef)) ())
((or (eq y2 'true)
(eq y2 t)) 'undef)
(t (list (cons y2 'false)))))
(eval (first x))
(second x)))))
(def s-cat (x y)
(cond ((not (is-string x))
(error '(s-cat applied to non-string) x))
((not (is-string y))
(error '(s-cat applied to non-string) y))
(t (list 'string (append (second x) (second y))))))
(def firstch (x)
(cond ((not (is-string x)) (error '(firstch of non-string)x))
((atom (second x)) (error '(firstch of emptystring)x))
(t (first (second x)))))
(def tail (x)
(cond ((not (is-string x)) (error '(tail of non-string) x))
((atom (second x)) (error '(tail of emptystring)x))
(t (list 'string (rest (second x))))))
(def s-cons (x y)
(cond ((not (eq (flatc x) 1)) (error '(bad character object/, s-cons) x))
((not (is-string y)) (error '(s-cons of non-string) y))
(t (list 'string (cons x (second y))))))
(def mk-string (x) (cond ((not (eq (flatc x) 1)) (error '(mk-string of non-character)
x))
(t (list 'string (cons x () )))))
(def is-list (l)
(cond ((atom l) (eq l nil))
(t (is-list (rest l)))))
(def firstsym fexpr (l) (matchterms (second l) (list 'quote (ratom))))
;(list (cons (second l) (ratom))))
(def firstexp fexpr (l) (matchterms (second l) (read)))
(def write (x) (print x) ())
)
'primdefs)
NIL) ;END OF MOTHER PROG2
;stuff needed all over
(setq $n 156)
(setq rpg-bug 315)
(setq ? 77)
(setq tab 11)
(setq period 56)
(setq dollar-sign 44)
(setq hot-cross-bun 26)
(setq comma 54)
(setq back-arrow 137)
(setq or-sym 37)
(setq and-sym 4)
(setq lpar 50)
(setq rpar 51)
(setq space 40)
(setq carriage_return 15)
(setq line_feed 12)
(def is_funapp ()
(prog (fname arglist) (return
(cond ((eq (typep nxtsym) 'symbol) (setq fname nxtsym)
(cond ((eq (setq nxtsym (ratom)) '/( )
(setq nxtsym (ratom))
(setq arglist (formalize
(readargs)))
(make_funapp fname arglist))
(t (error '(missing arglist) nxtsym))))
(t (error '(funapp with bad function name) nxtsym))))))
;no infix function applications are allowed in this version
(def readargs ()
(prog (arg)
(cond ((eq nxtsym '/,) (setq nxtsym (ratom))))
(return (cond ((eq nxtsym '/) ) (setq nxtsym (ratom)) ())
((eq (tyipeek) lpar) (cons (is_funapp) (readargs)))
((eq nxtsym '/() (cond ((eq (setq nxtsym (ratom)) '/))
(setq arg ())
(setq nxtsym (ratom))
(cons arg (readargs)))
(t (error '(unquoted non-empty list as arg)nxtsym))))
((atom nxtsym) (setq arg nxtsym) (setq nxtsym (ratom))
(cons arg (readargs)))
((eq (first nxtsym) 'quote) (setq arg nxtsym) (setq nxtsym (ratom))
(cons arg (readargs)))
((eq (first nxtsym) 'string) (setq arg nxtsym) (setq nxtsym (ratom))
(cons arg (readargs)))
(t (error '(weird argument) nxtsym))))))
(def make_funapp (x y) (cons x y))
(def ratom () (setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym tab) (eq nxtsym carriage_return))))
(setq nxtsym (readch))
(setq nxtsym (tyipeek)))
(cond ((or (eq nxtsym comma) (eq nxtsym back-arrow) (eq nxtsym period)
(eq nxtsym or-sym) (eq nxtsym and-sym)
(eq nxtsym lpar) (eq nxtsym rpar)) (setq nxtsym (readch)))
(t (setq nxtsym (read))
(cond ((eq nxtsym 'true) t)
((eq nxtsym 'f) 'false)
(t nxtsym)))))
(def first (x) (car x))
(def second (x) (cadr x))
(def third (x) (caddr x))
(def fourth (x) (cadddr x))
(def rest (x) (cdr x))
(def is_fundef ()
(cond ( (eq nxtsym 'function)
(setq fname (read))
(princ '|/
input pattern? |)
(setq nxtsym (tyipeek))
(do () ((not (eq nxtsym ?)))
(setq nxtsym (readch))
(princ '|/
/
The input pattern is a list of 1's and 0's (optionally separated /
by commas) indicating which of the parameters are to be considered/
input (values available on procedure call) and which are output/
(values to be computed)/, respectively. For example/,/
"(1/, 1/, 0)"/
indicates that the last parameter is thought of as a function/
of the first two parameters./
/
input pattern? |)
(setq nxtsym (tyipeek)))
(setq inpat (read))
(princ '|/
parameter list?/ |)
; (cond ((not inflag) (readch)(readch)))
(readch)(readch)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) )))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
the parameter list is a list of variables, enclosed in parentheses,/
and optionally separated by commas. /
For example, "(x1, x2, x3)" |)
(terpri)(princ '|/
parameter list?/ |)
(cond ((not inflag) (readch)(readch)))
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) )))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
(cond ((eq nxtsym carriage_return)
(setq params (make-up-args inpat))
(setq precond t)
(setq postcond t)
(princ '|/
you've just defaulted on formal parameters, precondition,/
and postcondition, you know that really is not a good idea./
/
body? |))
((eq nxtsym lpar)
(setq params (formalize (read)))
(princ '|/
precond?/ |)
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
a precondition is a disjunction, which expresses a condition /
or domain over which the function being defined is guaranteed/
to terminate. The disjunction must be terminated by a period.|) (terpri)
(princ '| /
domain-spec ::= disjunction "."/
/
disjunction ::= conjunction /| disjunction "∨" conjunction /
/
conjunction ::= literal /| conjunction "∧" literal /
/
literal ::= atomic-formula /| "¬" atomic-formula /
/
atomic-formula ::= "true" /| fun-app /| "(" disjunction ")" /
/
fun-app ::= name arglist /
/
arglist ::= "( )" /| "(" args ")"/
/
args ::= arg /| arg "," args /
/
arg ::= identifier /| number /| fun-app /
/
For example, "integer(x1,y) ∧ grtr-eq(x1,0,z)" /
Don't forget to include the output variables, in this case y and z.
|)
(terpri)(terpri)(princ '|precond? |)
(setq nxtsym (ratom)))
(setq precond (readspec))
(princ '|/
postcond?/ |)
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
A postcondition is a disjunction, which expresses a condition /
guaranteed to be true of the output variables. It might also/
be considered as a specification of the range of the function.|)
(princ '| /
range-spec ::= disjunction "."/
/
disjunction ::= conjunction /| disjunction "∨" conjunction /
/
conjunction ::= literal /| conjunction "∧" literal /
/
literal ::= atomic-formula /| "¬" atomic-formula /
/
atomic-formula ::= "true" /| fun-app /| "(" disjunction ")" /
/
fun-app ::= name arglist /
/
arglist ::= "( )" /| "(" args ")"/
/
args ::= arg /| arg "," args /
/
arg ::= identifier /| number /| fun-app /
/
For example, "integer(y,z) ∧ grtr(y,0,z)" /
(remember the output variables!)/
|)
(terpri)(princ '|/
postcond?/ |)
(setq nxtsym (ratom)))
(setq postcond (readspec))
(princ '|/
body?/ |))
(t (error '(no "/(" seen when asking for parameters) nxtsym)))
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
A function body is a set of horn clauses, terminated by a period./
/
body ::= horn-clauses "."/
/
horn-clauses ::= h-clause /| h-clause horn-clauses/
/
h-clause ::= goal "←" subgoals /| goal/
/
goal ::= fun-app/
/
subgoals ::= fun-app /| fun-app "," subgoals/
/
fun-app ::= name arglist /
/
For example:/
/
fact(0,1)/
fact(n,z) ← sub1(n,x), fact(x,z1), times(n,z1,z)/
|)
(terpri)(princ '|/
body?/ |)
(setq nxtsym (ratom)))
(setq body (repclauses)))
(t nil)))
(def make-up-args (list)
(cond ((null list) ())
(t (cons (gensym) (make-up-args (rest list))))))
(def is-gendef ()
(prog (specs gname params bodies-pair)
(return
(cond ( (eq nxtsym 'generic)
(setq gname (read))
(princ '|/
parameter list?/ |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
the parameter list is a list of variables, enclosed in parentheses,/
and optionally separated by commas. /
For example, "(x1, x2, x3)" |)
(terpri)(princ '|/
parameter list?/ |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
(setq params (formalize (read)))
(princ '|/
choices? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
a choice consists of an input pattern, function-name, precondition, postcondition,
and body-name. Just give the input pattern and the system will ask you for the
rest./
/
/
if there are no more choices to be entered type "."/
/
choices? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
(prog (fun-name inpat precond postcond body-name)
(setq specs
(do ( (selections () (cons (cons inpat fun-name) selections))
(flag () ()) ;flag tells whether fun-name is new
(bodies () (cond (flag (cons body-name bodies))
(t bodies)))
(fun-names () (cond (flag
(cons fun-name fun-names))
(t fun-names))) )
( (eq nxtsym period)
(setq nxtsym (ratom))
(cons selections (cons bodies fun-names)) )
(setq inpat (read))
(princ '|/
function name? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
this is the name the system will use to define a function with the given input
pattern, to be called whenever a generic call is made which fits the input-
pattern/
/
function name? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
(setq fun-name (read))
(cond
((get fun-name 'body) nil);if it is already defined, do nothing
((eq '% (first (explode fun-name)))
(autopred fun-name params)); if system function, autopred it
(t ;otherwise, get the rest of the info
(setq flag t)
(putprop fun-name inpat 'inpat)
(putprop fun-name params 'params)
(princ '|/
precond?/ |)
(setq nxtsym (ratom))
(cond ((eq nxtsym 'precond?) (setq nxtsym (ratom))))
(do ()((not (eq nxtsym '?)))
(princ '|/
a precondition is a disjunction, which expresses a condition /
or domain over which the function being defined is guaranteed/
to terminate. The disjunction must be terminated by a period.|) (terpri)
(princ '| /
domain-spec ::= disjunction "."/
/
disjunction ::= conjunction /| disjunction "∨" conjunction /
/
conjunction ::= literal /| conjunction "∧" literal /
/
literal ::= atomic-formula /| "¬" atomic-formula /
/
atomic-formula ::= "true" /| fun-app /| "(" disjunction ")" /
/
fun-app ::= name arglist /
/
arglist ::= "( )" /| "(" args ")"/
/
args ::= arg /| arg "," args /
/
arg ::= identifier /| number /| fun-app /
/
For example, "integer(x1,y) ∧ grtr-eq(x1,0,z)" /
Don't forget to include the output variables, in this case y and z.
|)
(terpri)(terpri)(princ 'precond? )
(setq nxtsym (ratom))
(cond ((eq nxtsym 'precond?) (setq nxtsym
(ratom)))))
(setq precond (readspec)) (putprop fun-name precond 'precond)
(princ '|/
postcond?/ |)
(setq nxtsym (ratom))
(cond ((eq nxtsym 'postcond?) (setq nxtsym (ratom))))
(do ()((not (eq nxtsym '?)))
(princ '|/
A postcondition is a disjunction, which expresses a condition /
guaranteed to be true of the output variables. It might also/
be considered as a specification of the range of the function.|)
(princ '| /
range-spec ::= disjunction "."/
/
disjunction ::= conjunction /| disjunction "∨" conjunction /
/
conjunction ::= literal /| conjunction "∧" literal /
/
literal ::= atomic-formula /| "¬" atomic-formula /
/
atomic-formula ::= "true" /| fun-app /| "(" disjunction ")" /
/
fun-app ::= name arglist /
/
arglist ::= "( )" /| "(" args ")"/
/
args ::= arg /| arg "," args /
/
arg ::= identifier /| number /| fun-app /
/
For example, "integer(y,z) ∧ grtr(y,0,z)" /
(remember the output variables!)/
|)
(terpri)(princ '|/
postcond?/ |)
(setq nxtsym (ratom))
(cond ((eq nxtsym 'postcond?)
(setq nxtsym (ratom)))))
(setq postcond (readspec)) (putprop fun-name postcond 'postcond)
(princ '|/
body-name? |)
(cond ((not inflag) (ratom)))
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
this is the name which associates the proper body definition with the function
being defined/
/
body-name?/ |)
(cond ((not inflag) (ratom)))
(setq nxtsym (ratom)))
(setq body-name nxtsym)
(putprop fun-name body-name 'bodyname)
));end of cond for defining fun-name
(princ '|/
choices? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(do ()((not (eq nxtsym ?)))(setq nxtsym (readch))
(princ '|/
a choice consists of an input pattern, function-name, precondition, postcondition,
and body-name. Just give the input pattern and the system will ask you for the
rest./
/
if there are no more choices to be entered type "."/
/
choices? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek))))
)))
;end of the "do" that gets all the choices and the setq of the result of "do"
;and the prog surrounding it
(print (make-gendef gname (reverse (first specs))))
(cond ((first (rest specs))
(setq bodies-pair (splitbodies (second specs) '(()()) ))
(setq namelist (append (rest (rest specs)) namelist))
(princ '|/
body-defs:|)
(prog (bodnam fun-name genrlflag genrldef)
(do ( (rep-bodies (second bodies-pair) rep-bodies)
(donebods () (cons bodnam donebods))
(fun-names (reverse (rest (rest specs))) (rest fun-names))
(rep-defs () (cond ((and genrlflag (not (member
bodnam donebods)))
(cons (cons bodnam genrldef) rep-defs))
(t rep-defs))) )
((null fun-names))
(setq fun-name (first fun-names))
(setq bodnam (get fun-name 'bodyname))
(setq genrlflag (member bodnam rep-bodies))
(cond ((member bodnam donebods) (spec-def fun-name
(getdef bodnam rep-defs)))
(t
(terpri)
(princ bodnam)
(princ '|? |)
(setq nxtsym (tyipeek))
(do () ((not (or (eq nxtsym space) (eq nxtsym line_feed)
(eq nxtsym carriage_return))))
(setq nxtsym (readch)) (setq nxtsym (tyipeek)))
(setq nxtsym (ratom))
(do ()((not (eq nxtsym '?)))
(princ '|/
A function body is a set of horn clauses, terminated by a period./
/
body ::= horn-clauses "."/
/
horn-clauses ::= h-clause /| h-clause horn-clauses/
/
h-clause ::= goal "←" subgoals /| goal/
/
goal ::= fun-app/
/
subgoals ::= fun-app /| fun-app "," subgoals/
/
fun-app ::= name arglist /
/
For example:/
/
fact(0,1)/
fact(n,z) ← sub1(n,x), fact(x,z1), times(n,z1,z)/
|)
(terpri)
(princ bodnam)
(princ '|? |)
(setq nxtsym (ratom))
(cond ((eq nxtsym (implode (append
(explode bodnam)
'(?))))
(setq nxtsym (ratom)))))
(setq inpat (get fun-name 'inpat))
(putprop fun-name
(cond (genrlflag
(setq genrldef (repclauses))
(spec-def fun-name genrldef))
(t (repclauses)))
'body) )))) ;end of do collecting body-defs
(make-fundefs (rest (rest specs))))) ;end of conditional on bodies
(print 'end_of_generic_spec) (terpri) (terpri)
t) ;end first clause of cond
(t nil)))))
;(def intersect (pat1 pat2)
; (cond ((null pat1) () )
; (t (cons (times (first pat1) (first pat2))
; (intersect (rest pat1) (rest pat2))))))
;(def addnew (name list)
; (cond ((member name list) list)
; (t (cons name list))))
(def make-gendef (name sel-list)
(putprop name sel-list 'generic))
(def make-fundefs (fun-names)
(cond
((null fun-names) t)
(t
((lambda (x) (eval x)
(eval (list 'grindef (first fun-names))))
(translate (first fun-names) target))
(putprop (first fun-names) t 'function)
(terpri) (terpri)
(make-fundefs (rest fun-names)))))
(def splitbodies (bods ans)
(cond ((null bods) ans)
(t (splitbodies (rest bods)
(checkbod (first bods) ans)))))
(def checkbod (bodnam uniq-n-repeats)
(cond ((member bodnam (first uniq-n-repeats))
(list (first uniq-n-repeats)
(cons bodnam (second uniq-n-repeats))))
(t (list (cons bodnam (first uniq-n-repeats))
(second uniq-n-repeats)))))
(def getdef (name deflist)
(cond ((null deflist) (error '(looking for a genrl definition that does no exist) name))
((eq name (first (first deflist)))
(rest (first deflist)))
(t (getdef name (rest deflist)))))
(def spec-def (fun-name genrldef)
(cons 'bktrkcond (spec-altlist (rest genrldef) (get fun-name 'inpat))))
(def spec-altlist (genalts inpat)
(cond ((null genalts) ())
(t ((lambda (matchlist)
(setq knownvars (known-of matchlist inpat))
(cons (list matchlist
(cons 'try (spec-goals (goal-pt (first genalts)))))
(spec-altlist (rest genalts) inpat)))
(match-pt (first genalts))))))
(def goal-pt (alternative) (rest (second alternative)))
(def spec-goals (gengoals)
(prog (tempgoal choices)
(return (cond ((null gengoals) ())
((setq choices
(is-generic (setq tempgoal (first gengoals))))
(cons (choosefun tempgoal choices)
(spec-goals (rest gengoals))))
(t (cons tempgoal (spec-goals (rest gengoals))))))))
(def formalize (arglist)
(cond ((null arglist) ())
((is-var (first arglist))
(cons (implode (cons '! (explode (first arglist))))
(formalize (rest arglist))))
(t (cons (first arglist) (formalize (rest arglist))))))
; ((is-constant (first arglist))
; (cons (first arglist) (formalize (rest arglist))))
; (t (cons (cons (first (first arglist))
; (formalize (rest (first arglist))))
; (formalize (rest arglist))))))
(def is-typedef ()
(cond ((eq nxtsym 'type)
(setq typename (read))
(terpri)
; (princ '|/
;basis-elements?/ |)
; (readch)(readch)
; (setq nxtsym (tyipeek))
; (do ()((not (eq nxtsym ?))) (setq nxtsym (readch))
; (princ '|/
;If one intends to define a type inductively then one must/
;specify the basis elements of the type. /
;This is done by giving a list of basis elements. /
; For example, "(empty-tree)"./
; /
;This is optional, as all data types need not be defined /
;inductively. A carriage-return in reply to "basis-elements?"/
;ndicates that none are to be given/
;)
; (terpri)(princ '|/
;asis-elements?/ |)
; (readch)(readch)
; (setq nxtsym (tyipeek)))
; (cond ((not (eq nxtsym carriage_return))
; (setq basis-element-list (append (read) basis-element-list))
; (princ '|/
;constructor-list?/ |)
; (readch)(readch)
; (setq nxtsym (tyipeek))
; (do () ((not (eq nxtsym ?)))(setq nxtsym (readch))
; (princ '|/
;The constructor-list is simply a list of the constuctors/
;used to create new elements of the data type from other elements./
; For example, "(graft)" /
;for the data type "tree"./
;Note that this is simply a list of the constructor names and /
;does not include argument lists./
;|)
; (terpri)(princ '|/
;constructor-list?/ |)
; (readch)(readch)
; (setq nxtsym (tyipeek)))
; (cond ((eq nxtsym carriage_return) (setq nxtsym (readch))
; (princ '|/
;Given that there are basis elements, we assume an inductive/
;definition is to be given. Therefore one MUST also give a /
;constructor for the data type. /
;|) (terpri)
; (princ '|/
;constructor-list?/ |)
; (readch)
; (setq nxtsym (tyipeek))))
; (cond ((eq nxtsym ?)(setq nxtsym (readch))
; (princ '|/
;The constructor-list is simply a list of the constuctors/
;used to create new elements of the data type from other /
;elements./
; For example, "(graft)" /
;for the data type "tree"./
;Note that this is simply a list of the constructor names /
;and does not include argument lists./
;|)
; (terpri)(princ '|/
;constructor-list?/ |)
; (readch)(readch)
; (setq nxtsym (tyipeek))))
; (cond ((eq nxtsym lpar)
; (setq constructor (read))
; (put-types constructor)
; (setq constructor-list
; (append constructor constructor-list)))
; (t (error '(no constructor-list following basis-list)
; nxtsym)))))
(setq params '(!x !y))
(setq inpat '(1 0))
(setq precond t)
(setq postcond '(boolean !y t))
(princ '|/
body?/ |)
(setq nxtsym (ratom))
(do () ((not (eq nxtsym '?)))
(princ '|/
For a type definition, the input pattern is always (1 0), the/
precondition is true, and the postcondition is that the output/
variable will have a boolean value./
/
A type body is a set of horn clauses,terminated by a/
period; it can be considered as the definition of a/
function to test for membership in the type. It /
always has a single input variable, which can be /
anything, and a single output variable, which is /
always truth-valued./
/
body ::= horn-clauses "."
/
horn-clauses ::= h-clause /| h-clause horn-clauses/
/
h-clause ::= goal "←" subgoals /| goal/
/
goal ::= fun-app/
/
subgoals ::= fun-app /| fun-app "," subgoals/
/
fun-app ::= name arglist /
/
For example:/
tree(empty-tree,y)/
tree( graft(t1,t2), y) ← tree(t1,y1), tree(t2,y2)/
|)
(terpri)(princ '|/
body?/ |)
(setq nxtsym (ratom)))
(setq body (repclauses)))
(t nil)))
(def put-types (l)
(cond ((null l) t)
(t (putprop (first l) typename 'typename)
(put-types (rest l)))))
(def readspec ()
(prog (disj)
(return (cond ((setq disj (is_disjunct)) disj)
(t (error (specification is not disjunction) nxtsym))))))
(def is_disjunct ()
(prog (conj1 conj2) (return
(cond ((setq conj1 (is_conjunct))
(do () ((not (eq nxtsym '∨)) conj1)
(setq nxtsym (ratom))
(cond ((setq conj2 (is_conjunct))
(setq conj1 (make_or conj1 conj2)))
(t (error '(∨ not followed by conjunct) nxtsym)))))
(t (error '(no conjunct to start with) nxtsym))))))
(def make_or (x y) (list '∨ x y))
(def make_and (x y) (list '∧ x y))
(def is_conjunct ()
(prog (lit1 lit2) (return
(cond ((setq lit1 (is_literal))
(do () ((not (eq nxtsym '∧)) lit1)
(setq nxtsym (ratom))
(cond ((setq lit2 (is_literal))
(setq lit1 (make_and lit1 lit2)))
(t (error '(∧ not followed by literal) nxtsym)))))
(t (error '(no literal to start with) nxtsym))))))
;(def is_literal ()
; (prog (atm) (return
; (cond ((eq nxtsym '¬) (setq nxtsym (ratom))
; (cond ((setq atm (is_atmf)) (make_not atm))
; (t (error '(¬ followed by non-atomf) nxtsym))))
; ((setq atm (is_atmf)) atm)
; (t (error '(no atm for literal) nxtsym))))))
;(def make_not (x) (list 'not x))
(def is_literal ()
(prog (atmf) (return
(cond ((or (eq nxtsym t) (eq nxtsym 'true)) (setq nxtsym (ratom)) t)
((eq nxtsym '/( ) (setq nxtsym (ratom))
(cond ((setq atmf (is_disjunct))
(cond ((eq nxtsym '/) )
(setq nxtsym (ratom))
atmf)
(t (error '(missing right paren) nxtsym))))
(t (error '(no disjunct in parens) nxtsym))))
(t (is_funapp))))))
(def repclauses ()
(cons 'bktrkcond (read_alternatives)))
; (cond ((reg-cond altlist) (cons 'cond altlist))
; (t (cons 'bktrkcond altlist))))
(def read_alternatives ()
(cond ((eq nxtsym '/.) ())
(t (cons (is_alternative) (read_alternatives)))))
;"←" should only appear in clauses which have something to the right of it
(def is_alternative ()
(do ()((not (eq nxtsym '?)))
(princ '|/
You are in the midst of specifying the body, a horn clause is looked for./
Don't forget that a single-goal clause does NOT have "←" following the goal,/
and the commas which separate subgoals are mandatory./
Here is a grammar description:/
/
horn-clauses ::= h-clause /| h-clause horn-clauses/
/
h-clause ::= goal "←" subgoals /| goal/
/
goal ::= fun-app/
/
subgoals ::= fun-app /| fun-app "," subgoals/
/
fun-app ::= name arglist /
/
|)
(terpri)(princ '|/
horn-clause?/ |)
(setq nxtsym (ratom)))
(cond ((setq goal (is_funapp))
(setq known-vars (known-of (rest goal) inpat))
(list (rest goal) (make_try (list_subgoals))))
(t (error '(bad goal) nxtsym))))
(def known-of (termlist pattern)
(cond ((null termlist) () )
((eq (first pattern) 1) (append (vars-in (first termlist))
(known-of (rest termlist)
(rest pattern))))
(t (known-of (rest termlist) (rest pattern)))))
(def vars-in (term)
(cond ( (atom term)
(cond ((is-var term)
(list term))
(t () )) )
( t (vars-in-list (rest term)))))
(def vars-in-list (termlist)
(cond ((null termlist) () )
(t (append (vars-in (first termlist))
(vars-in-list (rest termlist))))))
(def list_subgoals ()
(prog (tempgoal choices)
(return (cond ((eq nxtsym '←)
(setq nxtsym (ratom))
(setq tempgoal (is_funapp))
(cond ((and (not genrlflag)
(setq choices (is-generic tempgoal)))
(cons (choosefun tempgoal choices)(read_subgoals)))
((eq '% (first (explode (first tempgoal))))
(autopred (first tempgoal) (rest tempgoal))
(addoutvars tempgoal)
(cons tempgoal (read_subgoals)))
((not (null tempgoal))
(addoutvars tempgoal)
(cons tempgoal (read_subgoals)))
(t (error '(subgoal is not a funapp) nxtsym))))
(t ())))))
(def is-generic (call) (get (first call) 'generic))
(def addoutvars (call)
(do ((pat (get (first call) 'inpat) (rest pat))
(varlist (rest call) (rest varlist)))
((null pat))
(cond ((eq (first pat) 0)
(setq known-vars (append (vars-in (first varlist))
known-vars))))))
(def choosefun (call choicelist)
(prog (pat fun)
(setq pat (mk-pat (rest call)))
(setq fun (findfun pat choicelist))
(addoutvars (cons fun (rest call)))
(return (cons fun (rest call)))))
(def mk-pat (varlist)
(cond ((null varlist) () )
((is-constant (first varlist))
(cons 1 (mk-pat (rest varlist))))
((is-var (first varlist))
(cond ((memq (first varlist) known-vars)
(cons 1 (mk-pat (rest varlist))))
(t (cons 0 (mk-pat (rest varlist))))))
((all-vars-known (first varlist))
(cons 1 (mk-pat (rest varlist))))
(t (cons 0 (mk-pat (rest varlist))))))
(def findfun (key pairlist)
(cond ((null pairlist)
(princ '| /
i can't figure out which function you want from context, please help./
the patterns and function names you've given me are:/
|) (princ choicelist) (princ '|/
known-vars is: |) (princ known-vars) (princ '|/
which function do you want? |)
(read))
((as-defined-as key (first (first pairlist)))
(rest (first pairlist)))
(t (findfun key (rest pairlist)))))
(def as-defined-as (pat1 pat2)
(cond ((null pat1) t)
((and (eq (first pat1) 0) (eq (first pat2) 1)) nil)
(t (as-defined-as (rest pat1) (rest pat2)))))
(def all-vars-known (exp)
(cond ((atom exp) (or (is-constant exp)
(memq exp known-vars)))
(t (all-vars-in-list-known (rest exp)))))
(def all-vars-in-list-known (l)
(cond ((null l) t)
((all-vars-known (first l))
(all-vars-in-list-known (rest l)))
(t nil)))
(def make_match (x y) (list 'match x y))
(def make_try (l) (cons 'try l))
(def read_subgoals ()
(prog (tempgoal choices)
(return (cond ((eq nxtsym '/,)
(setq nxtsym (ratom))
(setq tempgoal (is_funapp))
(cond ((and (not genrlflag)
(setq choices (is-generic tempgoal)))
(cons (choosefun tempgoal choices)(read_subgoals)))
((eq '% (first (explode (first tempgoal))))
(autopred (first tempgoal) (rest tempgoal))
(addoutvars tempgoal)
(cons tempgoal (read_subgoals)))
((not (null tempgoal))
(addoutvars tempgoal)
(cons tempgoal (read_subgoals)))
(t (error '(subgoal is not a funapp) nxtsym))))
(t ())))))
;this is to check the argument positions in each alternative clause to
;determine whether the alternatives are mutually exclusive in any
;instance and thus a regular conditional may be used instead of the
;"backtracking" conditional.
;(def reg-cond (alternatives) nil)
;(def reg-cond (alternatives)
; (cond ((null alternatives) t)
; ((ck_excl (first alternatives) (rest alternatives))
; (reg-cond (rest alternatives)))
; (t nil)))
;(def ck_excl (alt listalts)
; (cond ((null listalts) t)
; ((excl_args (argpt alt) (argpt (first listalts)))
; (ck_excl alt (rest listalts)))
; (t nil)))
;
;
;def argpt (alternative) (third (first alternative)))
;
;
;def excl_args (list1 list2)
; (cond ((null list1) (cond ((null list2) nil)
; (t (error '(different length lists) list2))))
; (t (setq t1 (first list1))
; (setq t2 (first list2))
; (cond ((equal t1 t2) (excl_args (rest list1) (rest list2)))
; ((atom t1) (cond ((is-var t1) (cond ((is-constr-of t2 t1)
; t)
; (t (excl_args
; (rest list1)
; (rest list2)))))
;this clearly is not making much of an effort to find actual matches. I am only
;interested in when matches can definitely not exist. If I made substitutions as
;I went along, I would be able to find more of these cases but would certainly not
;invalidate any of the decisions made otherwise.
;
; (t (cond ((and (eq t1 0) (is-suc t2))
; t)
; ((contains-var t2)
; (excl_args
; (rest list1)
; (rest list2)))
; (t (cond
; ((equal t1 (eval t2))
; (excl_args
; (rest list1)
; (rest list2)))
; (t t)))))))
; ((atom t2) (cond ((is-var t2) (cond ((is-constr-of t1 t2)
; t)
; (t (excl_args
; (rest list1)
; (rest list2)))))
; (t (cond ((and (eq t2 0)(is-suc t1)) t)
;; ((contains-var t1)
; (excl_args
; (rest list1)
; (rest list2)))
; (t (cond
; ((equal t2 (eval t1))
; (excl_args
;; (rest list1)
; (rest list2)))
; (t t)))))))
; ((or (contains-var t1) (contains-var t2))
; (excl_args (rest list1) (rest list2)))
; ((equal (eval t1) (eval t2)) (excl_args (rest list1)
; (rest list2)))
; (t t)))))
;
(def is-constant (x)
(cond ((atom x) (or (numberp x)
(eq x t)
(eq x 'f)
(eq x 'true)
(eq x 'undef)
(eq x 'false)
(eq x nil)))
; (is-basis-element x)))
(t (or (not (is-string x)) (eq (first x) 'quote)
(not (contains-var x))))))
(def is-var (x) (and (atom x) (not (is-constant x))))
;(def is-basis-element (x) (memq x basis-element-list))
;(def is-constructor (x) (memq x constructor-list))
;(def is-constr-of (x y)
; (cond ((atom x) nil)
; (t (and (memq y (rest x)) (is-constructor (first x))))))
(def contains-var (exp)
(cond ((atom exp) (is-var exp))
(t (list-contains-var (rest exp)))))
;contains-var ignores function names when looking for variables since the only
;functions left in at this point are constructors
(def list-contains-var (explist)
(cond ((null explist) nil)
((contains-var (first explist)) t)
(t (list-contains-var (rest explist)))))
(def translate (name target)
(cond ((eq target 'lisp)
(make_lisp_def))
((eq target 'pascal)
(mk-strong-typed)
(make_pascal_def ))
(t (error '(language not yet implemented) target))))
(def make_lisp_def () (list 'defun name 'fexpr '(l)
(list 'cond (list
(list 'true-precond (list 'cons
(list 'quote
name)
'l))
(list 'bktrkcond
'l
(list 'quote (rest body))))
'(t 'undef))))
(def mk-strong-typed ()
(make-formal-types (get name 'params) ;this function puts the formal params
(get name 'precond) ;and their types under 'types, and
(get name 'postcond) ;deletes the type decs from the pre-
name) ;and post-conditions, putting the
;results under 'typedprecond and
;typedpostcond
(putprop name (append (extcalls (get name 'typedprecond))
(findprocs (rest (get name 'body)) name)) 'external-procs)
(putprop name (find-local-types (rest (get name 'body)) name) 'local-decs))
(def make-formal-types (params precond postcond name)
((lambda (split-pre split-post)
(putprop name (mk-param-types params
(append (first split-pre)
(first split-post)))
'types)
(putprop name (rest split-pre) 'typedprecond)
(putprop name (rest split-post) 'typedpostcond))
(findtypes precond)
(findtypes postcond)))
(def mk-param-types (params types)
(cond ((null params) ())
(t ((lambda (ans)
(cond ((defined ans)
(cons ans (mk-param-types (rest params)
types)))
(t (error '(has no type defined) (first params)))))
(lookup (first params) types)))))
(def lookup (var alist)
(cond ((null alist) 'undef)
((eq var (first (first alist)))
(rest (first alist)))
(t (lookup var (rest alist)))))
(def findtypes (precond) ;returns the dotted-pair: list of var-type pairs,
(cond ((atom precond) ;and non-type-dec part of precond
(cons () precond))
((is-or precond)
(error '(no ∨'s allowed in preconditions when translating
to strongly typed languages) precond))
;if we switch from dnf to cnf, then we can allow ∨'s to appear
;in pre- and post-conditions, but no type decs may be ∨'ed, the
;alternative replacing the error above would be:
;(cons () precond)
((is-and precond)
((lambda (rest-ans1 rest-ans2)
(cons (append (first rest-ans1)
(first rest-ans2))
(list '∧ (rest rest-ans1)
(rest rest-ans2))))
(findtypes (second precond))
(findtypes (third precond))))
((is-type (first precond)) ;we know that the first
(cons (list (cons (second precond) ;argument of a type
(first precond))) ;app. is the input var
T))
(t (cons () precond)))) ;o.w. it is a condition to be checked
(def is-type (name)
(or (get name 'type)
(memq name prim-types)))
(def extcalls (wff)
(cond ((atom wff) ())
(t (cond ((or (eq (first wff) '∧)
(eq (first wff) '∨))
(append (extcalls (second wff))
(extcalls (third wff))))
(t (list (first wff)))))))
(def findprocs (alts name)
(cond ((null alts) ())
(t (append (findcalls (try-pt (first alts)) name)
(findprocs (rest alts) name)))))
(def findcalls (sbgls name)
(cond ((null sbgls) ())
(t ((lambda (procname)
(cond ((eq procname name)
(findcalls (rest sbgls) name))
(t (cons procname (findcalls (rest sbgls) name)))))
(first (first sbgls))))))
(def find-local-types (alts name)
(cond ((null alts) ())
(t (append (findtypesfor (try-pt (first alts)) name)
(find-local-types (rest alts) name)))))
(def findtypesfor (sbgls name)
(cond ((null sbgls) ())
(t ((lambda (sbgl)
(cond ((eq (first sbgl) name)
(findtypesfor (rest sbgls) name))
(t (append (make-type-list (rest sbgl)
(get (first sbgl) 'types))
(findtypesfor (rest sbgls) name)))))
(first sbgls)))))
(def make-type-list (actuals type-pattern) ;returns a list of var-type pairs
(cond ((null actuals) ())
((is-var (first actuals))
(cons (cons (first actuals)
(first type-pattern))
(make-type-list (rest actuals)
(rest type-pattern))))
((is-constant (first actuals))
(make-type-list (rest actuals)
(rest type-pattern)))
(t (append ;it's a funapp, i.e., a constructed type, so
(hard-type-list (first actuals) ;lookup def of type and make
(first type-pattern)) ;sure the constructor
(make-type-list (rest actuals) ;is appropriate, then find
(rest type-pattern)))))) ;types of the args
(def hard-type-list (exp type)
(cond ((eq (vars-in exp) ()) ())
(t ((lambda (bod)
(cond (bod (srch-alts (list exp (gensym)) ;assumes inpat (1 0)
(rest bod)))
(t (error '(has not yet been defined) type))))
(get type 'body)))))
(def srch-alts (actuals list-alts)
(cond ((null list-alts) (error '(has vars whose types I am unable to determine)
(first actuals)))
(t ((lambda (sbgls)
(cond ((defined sbgls)
((lambda (typedecs)
(cond ((null typedecs)
(srch-alts actuals
(rest list-alts)))
(t ((lambda (ans)
(cond ((all-typed
(vars-in (first actuals))
ans)
ans)
(t (srch-alts actuals
(rest list-alts)))))
(find-var-types
(vars-in (first actuals))
(append (first sbgls)
typedecs))))))
(find-type-decs (rest sbgls))))
(t (srch-alts actuals (rest list-alts)))))
(half-eval actuals (first list-alts))))))
(def half-eval (actuals alt) ;returns a substitution and list of subgoals with the
((lambda (sub) ;substitutions made
(cond ((defined sub)
(cons sub (mk-subst (try-pt alt) sub)))
(t 'undef)))
(match actuals (match-pt alt))))
(def find-type-decs (sbgls)
(cond ((null sbgls) ())
(t ((lambda (sbgl)
(cond ((is-type (first sbgl))
(append (make-type-list (list (second sbgl))
(list (first sbgl)))
(find-type-decs (rest sbgls))))
(t (find-type-decs (rest sbgls)))))
(first sbgls)))))
(def find-var-types (vars sub)
(cond ((null vars) ())
(t (cons (cons (first vars)
(lookup* (first vars) sub))
(find-var-types (rest vars) sub)))))
(def all-typed (vars alist)
(cond ((null vars) t)
((is-type (lookup (first vars) alist))
(all-typed (rest vars) alist))
(t nil)))
;top level
(def top ()
(prog (you-want-to-save)
; the next two lines should eventually be deleted
(setq target 'lisp)
(makedefs (get 'lisp 'primdefs))
(setq namelist ())
(setq inflag t)
;(setq basis-element-list () )
;(setq constructor-list () )
(setq prim-types '(integer real boolean is-string is-list))
(princ '|Hello, this is a program synthesis system which takes logic/
specifications as input and generates a program in the target/
language of your choice./
(Right now that choice is limited to LISP and maybe PASCAL). /
/
If you wish the output to go to a file, please give me the name/
of that file; if not, just hit carriage-return/
|)
(readch)(readch)
((lambda (filename)
(cond ((eq filename carriage_return) (setq outflag nil))
(t (setq outputfile (read))
; (setq outfiles (list (open (list '(dsk (j red)) filename 'gen) 'out)))
(uwrite dsk (j red))
(setq outflag t)
(setq ↑r t))))
(tyipeek))
(princ '|/
If you wish me to read specifications from a file you've created,/
then please give me the name of the file; if this session is to be/
interactive, then just hit carriage-return/
|)
(readch)(readch)
((lambda (filename)
(cond ((eq filename carriage_return) (setq inflag nil) (princ '|/
If you need help getting started, type "?"./
/
|))
(t (setq filename (read))
(setq inflag t)
(eval (list 'eread filename))
(setq ↑q t))))
(tyipeek))
(setq nxtsym (ratom))
(do () ((not (is_definition)) (print 'alldone))
(setq namelist (cons name namelist))
(putprop name params 'params)
(putprop name precond 'precond)
(putprop name inpat 'inpat)
(putprop name postcond 'postcond)
(putprop name body 'body)
((lambda (x) (cond ((eq target 'lisp)
(eval x) (eval (list 'grindef name)))
(t (unlist x))))
(translate name target))
(terpri)
(terpri)
(setq nxtsym (ratom)))
(cond (outflag
(eval (list 'ufile outputfile 'gen))))
(princ '|/
Do you want to save these internalized specifications on a file?/
If not, just hit carriage return... |)
(readch)
(readch)
(setq nxtsym (tyipeek))
(cond ((not (or (eq nxtsym carriage_return) (eq nxtsym $n)))
(setq you-want-to-save t) (setq nxtsym (read)))) ;you-want-to-save
(cond (you-want-to-save (princ '|/
on what file?/ |) ;is initialized to
;nil as prog var
((lambda (nam)
(dumpdefs namelist nam)
(princ '|/
Whenever you want to start the system up with these/
functions already defined as they were in this session,/
type/
"(include |)
(princ nam)(princ '|)"/
then type/
"(top)"/
Actually the call on include can take any number of/
filenames that you wish to include.|))
(read)))
(t (princ '|/
nothing saved/
|)))
(princ '|/
We now turn control back over to the top level of LISP. /
If you wish to start over type "(top)"/
|)))
(def is_definition ()
(do ()((not (eq nxtsym '?)))
(princ '|/
To specify the target language type:/
"target <language-name>"/
/
To specify a function definition type:/
"function <name>"/
followed by the rest of the specification. You will be asked for each/
part of the specification; if you don't know how to answer,/
type "?" for help./
/
To specify a generic function definition type:/
"generic <name>"/
followed by the rest of the specification. You will be asked for each/
part of the specification; if you don't know how to answer,/
type "?" for help./
/
To specify a data type type:/
"type <name>"/
followed by the rest of the specification. You will be asked for each/
part of the specification; if you don't know how to answer,/
type "?" for help./
/
To conclude the session type a period "."/
|)
(terpri)
(setq nxtsym (ratom)))
(setq genrlflag nil)
(cond ((is_fundef) (setq name fname)(putprop fname t 'function))
((is-gendef)(setq nxtsym (ratom)) (is_definition))
((is-typedef) (setq name typename)(putprop name t 'type))
((eq nxtsym 'target)(newtarget)(setq nxtsym (ratom))(is_definition))
((eq nxtsym '/.) nil)
(t (error '(bad start (or finish)) nxtsym))))
(def newtarget ()
(setq target (ratom))
(cond ((eq target 'lisp)
(setq deflist (get target 'primdefs))
(makedefs deflist))))
(def makedefs (dl) (cond ((null dl) t)
(t (eval (first dl)) (makedefs (rest dl)))))
(def dumpdefs (namelist filename)
(uwrite)
(setq ↑r t)
(setq ↑w t)
(do ((names namelist (rest names)))
((null names))
(prog (name)
(setq name (first names))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'params))
''params))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'precond))
''precond))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'postcond))
''postcond))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'inpat))
''inpat))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'body))
''body))
(print (list 'putprop (list 'quote name)
(list 'quote (get name 'fexpr))
''fexpr))
)) ;end of prog and do
(print ''*eof*)
(eval (list 'ufile filename 'ext))
(setq ↑w nil))
(def include fexpr (flnames)
(cond ((null flnames) 'all-done)
(t (eval (list 'eread (first flnames) 'ext))
(setq ↑q t)
(do ((x nil (eval (read))))
((eq x '*eof*)))
(eval (cons 'include (rest flnames))))))
(def unlist (l) (do ((dumplist l (rest dumplist)))
((null dumplist))
(cond ((eq (first dumplist) nil)
(princ '/( )(princ '/) ))
(t (princ (first dumplist))))))
;stuff needed for lisp to run generated programs
;(def bktrkcond (inpat actuals list-alts)
; (prog (answer$ flag outputvar)
; (setq outputvar (findout actuals inpat))
; (cond ((is-constant outputvar) (setq answer$ outputvar)
; (setq flag t)
; (setq outputvar (gensym))
; (setq actuals
; (exchgout actuals
; inpat outputvar))))
; (return (bktrkcond1 list-alts answer$ flag))))
;(def bktrkcond (outputvar actuals list-alts) (bktrkcond1 list-alts))
;(def bktrkcond fexpr (l) (bktrkcond1 l))
;(def bktrkcond1 (list-alts answer$ flag)
; (prog (x$ env outvar)
; ;outvar is local to bktrkcond1, set from original output-
;; var at the beginning of the attempt at each alternative
; (cond ((null list-alts) (return 'undef)))
; (setq outvar outputvar)
; (setq env (match actuals (matchgoal (first list-alts))))
; (cond ((defined env)
; (setq env (append env (chg-formals
; (rest (try-pt
; (first list-alts))))))
; (setq outvar (first (mk-subst (list outvar)env)))
; (setq x$ (eval (mk-subst
; (try-pt (first list-alts))
; env)))
; (cond ((defined x$)
; (return (cond (flag
; (cond ((equal answer$
; x$) x$)
; (t 'undef)))
; (t x$))))
; (t (return (bktrkcond1 (rest list-alts)
; answer$
; flag)))))
; (t (return (bktrkcond1 (rest list-alts)
; answer$
; flag))))))
;
;(def bktrkcond1 (list-alts)
; (prog (x$ env outvar flag answer$)
; ;outvar is local to bktrkcond1, set from original output-
; var at the beginning of the attempt at each alternative
; (cond ((null list-alts) (return 'undef)))
; (setq outvar outputvar)
; (setq env (match actuals (matchgoal (first list-alts))))
; (cond ((defined env)
; (cond ((is-constant outvar) (setq answer$ outvar)
; (setq flag t)))
; (setq env (append env (chg-formals
; (rest (try-pt
; (first list-alts))))))
;
; (setq outvar (first (mk-subst (list outvar)env)))
; (setq x$ (eval (mk-subst
; (try-pt (first list-alts))
; env)))
; (cond ((defined x$) (return x$
; (cond (flag
; (cond ((equal answer$
; x$) x$)
; (t 'undef)))
; (t x$))))
; )) ;only while above 5 lines are out
; (t (return (bktrkcond1 (rest list-alts))))))
; (t (return (bktrkcond1 (rest list-alts)))))))
(def bktrkcond (actuals list-alts)
(cond ((null list-alts) 'undef)
(t ((lambda (alt)
((lambda (answer-sub)
(cond ((defined answer-sub)
(cleanup answer-sub actuals))
(t (bktrkcond actuals (rest list-alts)))))
((lambda (sub)
(cond ((defined sub)
(append-if-defined sub
(try (mk-subst (try-pt alt)
sub))))
(t 'undef)))
(match actuals (match-pt alt)))))
(new-version (first list-alts))))))
(def new-version (alt)
((lambda (sub)
(list (mk-subst (match-pt alt) sub)
((lambda (newtry)
(cons 'try (mk-subst newtry (chg-formals newtry))))
(mk-subst (try-pt alt) sub))))
(chg-in (match-pt alt))))
(def chg-formals (sbgoals)
(cond ((null sbgoals) ())
(t ((lambda (x) (cond (x (append x (chg-formals (mk-subst
(rest sbgoals)
x))))
(t (chg-formals (rest sbgoals)))))
(chg-in (rest (first sbgoals)))))))
(def chg-in (params)
(cond ((null params) ())
;new stuff follows
((atom (first params))
(cond
;the next things used to be the whole shmeer
((eq (firstchar (first params)) '!)
((lambda (chg) (cons chg (chg-in (subst (cdr chg)
(car chg)
(rest params)))))
(cons (first params) (gensym))))
(t (chg-in (rest params)))))
;the rest is all new
((eq (first (first params)) 'quote)
(chg-in (rest params)))
(t ((lambda (chgs)
(append chgs (chg-in (mk-subst (rest params) chgs))))
(chg-in (rest (first params)))))))
(def firstchar (name)
(first (explode name)))
(def cleanup (sub actuals) (reverse (cleanup* sub actuals () )))
(def cleanup* (sub actuals ans)
(cond ((null actuals) ans)
(t ((lambda (act)
(cond ((is-var act)
(cond ((already-there act ans)
(cleanup* sub (rest actuals) ans))
(t (cleanup* sub (rest actuals)
(cons (cons act
(lookup* act sub))
ans)))))
((is-constant act)
(cleanup* sub (rest actuals) ans))
(t (cleanup* sub (rest actuals)
(cleanup* sub (rest act) ans)))))
(first actuals)))))
(def already-there (name alist)
(cond ((null alist) nil)
((eq name (var (first alist))) t)
(t (already-there name (rest alist)))))
(def lookup* (exp alist) ;makes all substitutions in alist that are
(do ((value (mk-subst exp alist) nxtval) ;applicable to exp
(nxtval (mk-subst (mk-subst exp alist) alist)
(mk-subst nxtval alist)) )
((equal value nxtval) value)))
(def try (subgoals)
(cond ((null subgoals) () )
; ((true-precond (first subgoals))
(t
( (lambda (sub)
(cond ((defined sub)
(append-if-defined sub
(try (mk-subst
(rest subgoals)
sub))))
(t 'undef)))
(eval (first subgoals)) ))
))
; (t 'undef)))
(def append-if-defined (sub1 sub2) ;when used in conjunction
(cond ((and (defined sub1) (defined sub2)) ;with "try", this involves
(append sub1 sub2)) ; a redundant test on the
(t 'undef))) ;first argument (who cares?)
;try makes use of the variable outvar which is bound inside and local to
;bktrkcond1, so one outvar is in effect for the execution of each alternative clause
;try makes use of the fact that we have decided to allow only typical implementation
;LISP functions, ones with a single output value.
;The value assigned to this
;variable by the computation must be propagated to all the rest of the clause, and
;to the outvar of the original goal.
;(def try fexpr (l)
; (try1 l))
;
;
;(def try1 (subgoals)
; (cond ((null subgoals) outvar) ;outvar need not be evaluated since its
; ;value is substituted in as it is found, not simply bound.
; ((true-precond (first subgoals)) (( lambda (l)
; (cond ((defined l)
; (prog (oldout)
; (setq oldout
; (getoldout
; (first subgoals)))
; (setq outvar
; (subst l oldout outvar))
; (return (try1 (subst l
; oldout
; (rest subgoals
; ))))))
; (t 'undef)))
; (eval (first subgoals))))
; (t 'undef)))
;
;
;(def getoldout (call)
; (do ((pat (get (first call) 'inpat) (rest pat))
; (arglist (rest call) (rest arglist)))
; ((or (null pat) (eq (first pat) 0))
; (cond ((null pat) nil)
; (t (first arglist))))))
;
(def true-precond (fnapp)
(prog (env2 ans-sub)
(setq env2 (bind (matchlis (first fnapp)) (rest fnapp)))
(setq ans-sub (evpred (mk-subst (get (first fnapp) 'precond) env2)))
(return (cond ((eq ans-sub ()) t)
((eq ans-sub 'undef) nil)
(t (error '(variables in precond check) ans-sub))))))
;precondition checker
(def evpred (f)
(cond ((atom f) (cond ((eq f t) ())
((eq f nil) (error '(no precondition exists for)
(first fnapp)))
(t (error '(weird atomic predicate)f))))
((is-or f) (evor (rest f)))
((is-and f) (evand (rest f)))
; ((is-not f) (evnot (evpred (rest f)))) ;not could be troublesome
;otherwise it is a pred-app
(t (eval f))))
; (t (cond ((no-funapp-terms (rest f)) (eval f))
; (t (error '(somehow a funapp term appeared in pred) f))))))
;weirdness here. Originally I thought that I had to worry about checking postcond-
;itions at this point in order to check preconditions. Now I think that the only
;place these will be used is in optimizing out the precondition check entirely in
;certain cases. Since function applications have been removed from terms by the
;front end business, they will never appear as terms in a precondition. The worst
;thing that can happen is an unbound variable appearing as input arg to a pred. I
;have a feeling that this will always come out true since the variable will match
;with anything. Worry about that later.
(def is-or (f) (eq (first f) '∨))
(def evor (l) (prog (val)
(setq val (evpred (first l)))
(return (cond ((eq 'undef val) (evpred (second l)))
((eq () val) ())
(t (evpred (second l))) ;who knows, we might as well let 'em try
(t (error '(evpred evaluates to something other than () or undef)
(cons val (first l))))))))
(def is-and (f) (eq (first f) '∧))
(def evand (l) (prog (val)
(setq val (evpred (first l)))
(return (cond ((eq val ()) (evpred (second l)))
((eq val 'undef) 'undef)
(t (error '(evpred evaluates to weirdness) (cons val (first l))
))))))
;(def is-not (f) (eq (first f) 'not))
;
;(def evnot (e) (cond ((eq e t) 'undef)
; ((eq e 'undef) t)
; (t (error '(evpred evaluates to weirdness) (cons e (rest f))))))
;
;
;(def no-funapp-terms (l)
; (cond ((null l) t)
; ((or (atom (first l))
; (memq (first (first l)) constructor-list))
; (no-funapp-terms (rest l)))
; (t nil)))
;
(def defined (x) (not (eq x 'undef)))
;bind is here creating an alist
(def bind (l1 l2)
(cond ((null l1) ())
(t (cons (cons (first l1) (first l2)) (bind (rest l1) (rest l2))))))
(def matchlis (fname) (get fname 'params))
;(def findout (arglist inpat)
; (cond ((null arglist) (error '(no outvar indicated) l1))
; ((eq (first inpat) 0) (first arglist))
; (t (findout (rest arglist) (rest inpat)))))
;
;
;def exchgout (arglist inpat newvar)
; (cond ((null arglist) (error '(no outvar indicated) l1))
; ((eq (first inpat) 0)
; (cons newvar (rest arglist)))
; (t (cons (first arglist) (exchgout (rest arglist)
; (rest inpat) newvar)))))
;
;(def match fexpr (l)
; (prog (l1 l2 l3)
; (setq l1 (evalinput-n-setoutvar (first l)))
; (setq l2 (second l))
; (setq l3 (match1 l1 l2))
; (return (cond ((defined l3) l3)
; (t 'undef)))))
;evalinput-n-setoutvar evaluates the input arguments and sets the variable outvar
;to the output variable. Outvar is global to match but local in bktrkcond1, so it
;has no side effects outside the scope of the current call on bktrkcond1.
;*** since all function applications (other than constructors) have been
;eliminated before this point, I believe it is unnecessary to evaluate any of the
;input arguments, they should be constants already. However, we do still need to
;set "outvar". Since the outvar does not change from clause to clause, but only
;from one procedure to the next, this can be done before any matches are attempted.
;i.e., the best place for it is as the first thing done by bktrkcond.
; I'll try it a new way and leave the old suff around as comments.
;(def evalinput-n-setoutvar (l)
; (cond ((null l) (error '(empty list of arguments)l))
; ((null (rest l)) (setq outvar (first l)) l )
; (t (cons (eval (first l)) (evalinput-n-setoutvar (rest l))))))
;stand-apart standardizes apart the lists l1 and l2, returning the list of
;substitutions to be made in l2 to accomplish this
;(def stand-apart (l1 l2)
; (prog (oldvar newvar rl)
; (setq rl (findvar l1 l2))
; (return (cond ((null rl) () )
;
; (t (setq oldvar (first rl))
; (setq rl (second rl))
; (setq newvar (intern (gensym)))
; (cons
; (cons oldvar newvar)
; (stand-apart rl
; (subst newvar oldvar l2))))))))
;
;
;findvar finds the first variable in l1 which also occurs in l2, and returns a list
;of 2 elements: 1) the variable found; 2) the remainder of the list l1, beginning
;with the element containing the first symbol past the variable found
; OR if no such variable can be found, it returns the empty list
;(def findvar (l1 l2)
; (cond
; ((null l1) () )
; (t (
; (lambda (x)
; (cond ((atom x)
; (cond ((and (is-var x) (occurs-in x l2))
; (list x (rest l1)))
; (t (findvar (rest l1) l2))))
; (t (
; (lambda (l)
; (cond ((null l) (findvar (rest l1) l2))
; (t (list (first l) l1))))
; (findvar x l2)
; ) )))
; (first l1)
; ) )))
;
;(def match1 (l1 l2)
; (prog (termatch)
; (return (cond ((null l1) (cond ((null l2) ())
; (t (error '(tried to match lists of unequal length)l2
; ))))
; (t (setq termatch (matchterms (first l1) (first l2)))
; (cond ((null termatch) (match1 (rest l1) (rest l2)))
; ((eq termatch 'undef) 'undef)
; (t (append
; termatch
; (match1 (mk-subst (rest l1) termatch) (mk-subst (rest l2)
; termatch))
; )) ))))))
(def match (l1 l2)
(prog (termatch)
(return (cond ((null l1) (cond ((null l2) ())
(t (error '(tried to match lists of unequal length)l2
))))
(t (setq termatch (matchterms (first l1) (first l2)))
(prog (restmatch)
(return
(cond ((null termatch) (match (rest l1) (rest l2)))
((eq termatch 'undef) 'undef)
((defined
(setq restmatch
(match (mk-subst (rest l1) termatch)
(mk-subst (rest l2) termatch))))
(append termatch restmatch))
(t 'undef)))) )))))
(def mk-subst (termlist alist) ;actually, termlist can be
(cond ((and (atom termlist)
(or (numberp termlist)
(eq termlist t)
(eq termlist 'f)
(eq termlist 'true)
(eq termlist 'undef)
(eq termlist 'false)
(eq termlist nil)))
termlist)
((and (not (atom termlist))
(or (not (is-string termlist)) (eq (first termlist) 'quote)))
termlist)
(t
(do ((l alist (rest l))
(exp termlist (subst (val (first l)) (var (first l)) exp)))
((null l) exp)))))
(def val (x) (cdr x))
(def var (x) (car x))
;all variables occurring in the terms to be matched are unbound, as substitutions
;are made as we go
(def matchterms (t1 t2)
(prog (f)
(return (cond ((equal t1 t2) ())
((atom t1) (cond ((is-var t1) (cond ((or (eq(is-string t2)())
(atom t2)) (cons
(cons t1 t2)
() ))
((occurs-in t1 t2)
(cond ((get
(setq f
(implode (append
(explode
'equal-bind-)
(explode
(get (first t2)
'typename)))))
'body)
(f t1 t2))
(t 'undef)))
(t (cons (cons t1 t2) ()))))
(t (cond ((is-var t2) (cons (cons t2 t1) ()))
((is-constant t1)
(cond ((atom t2) 'undef)
((and (eq (first t2) 'quote)
(eq (second t2) t1))
())
(t 'undef)))
((is-constant t2) 'undef)
((contains-var t2) (cond
((get
(setq f
(implode (append
(explode
'equal-bind-)
(explode
(get (first t2)
'typename)))))
'body)
(f t1 t2))
(t 'undef)))
((get
(setq f (implode (append
(explode
'equal-)
(explode
(get (first t2)
'typename)))))
'body)
(cond ((f t1 t2) ())
(t 'undef)))
(t 'undef)))))
((is-var t2) (cond
((eq (is-string t1) ())
(cons (cons t2 t1) () ))
((occurs-in t2 t1)
(cond ((get
(setq f
(implode (append
(explode
'equal-bind-)
(explode
(get (first t1)
'typename)))))
'body)
(f t1 t2))
(t 'undef)))
(t (cons (cons t2 t1) ()))))
((and (atom t2) (is-constant t2))
(cond ((and (eq (first t1) 'quote)
(eq (second t1) t2))
())
(t 'undef)))
((get (setq f (implode (append (explode 'equal-)
(explode (get (first t1)
'typename)))))
'body)
(cond ((f t1 t2) ())
(t 'undef)))
((or (and (not (eq (is-string t1) ()))(contains-var t1))
(and (not (eq (is-string t2) ()))(contains-var t2)))
(cond ((get (setq f (implode (append
(explode
'equal-bind-)
(explode
(get (first t1)
'typename)))))
'body)
(f t1 t2))
((and (eq (first t1) (first t2)) (not (eq (first t1) 'quote)))
(match (rest t1) (rest t2)))
((eq (first t1) 'list)
(matchterms (cons-out (rest t1)) t2))
((eq (first t2) 'list)
(matchterms (cons-out (rest t2)) t1))
((eq (first t1) 'cons)
(cond ((eq (first t2) 'quote)
((lambda (x)
(cond
((defined x)
((lambda (y)
(cond
((defined y)
(append x y))
(t 'undef)))
(matchterms
(mk-subst (third t1) x)
(list 'quote
(rest (second t2)) ))))
(t 'undef)))
(matchterms (second t1)
(list 'quote
(first (second t2))))))
(t
((lambda (x)
(cond
((defined x)
((lambda (y)
(cond
((defined y)
(append x y))
(t 'undef)))
(matchterms
(mk-subst (third t1) x)
(mk-subst (rest t2) x))))
(t 'undef)))
(matchterms (second t1) (first t2))))))
((eq (first t2) 'cons)
(cond ((eq (first t1) 'quote)
((lambda (x)
(cond
((defined x)
((lambda (y)
(cond
((defined y)
(append x y))
(t 'undef)))
(matchterms
(mk-subst (third t2) x)
(list 'quote
(rest (second t1)) ))))
(t 'undef)))
(matchterms (second t2)
(list 'quote
(first (second t1))))))
(t
((lambda (x)
(cond
((defined x)
((lambda (y)
(cond
((defined y)
(append x y))
(t 'undef)))
(matchterms
(mk-subst (third t2) x)
(mk-subst (rest t1) x))))
(t 'undef)))
(matchterms (second t2) (first t1))))))
(t 'undef)))
(t 'undef)))))
(def cons-out (l)
(cond ((null l) ())
(t (list 'cons (first l) (cons-out (rest l))))))
(def contains-var (exp)
(cond ((atom exp) (is-var exp))
(t (list-contains-var (rest exp)))))
;contains-var ignores function names when looking for variables since the only
;functions left in at this point are constant functions (arithmetic and constructors)
(def list-contains-var (explist)
(cond ((null explist) nil)
((contains-var (first explist)) t)
(t (list-contains-var (rest explist)))))
(def occurs-in (var exp)
(cond ((atom exp) (cond ((eq var exp) t)
(t nil)))
((occurs-in var (first exp)) t)
(t (occurs-in var (rest exp)))))
(def match-pt (alternative) (first alternative))
(def try-pt (alternative) (rest (second alternative)))
;*** automatic predicatizing ***
(def autopred (f varlist)
(cond
((get f 'body) nil) ;it's already defined, go away
(t
(putprop f (mk-params varlist) 'params)
(putprop f t 'precond) ;using system defined functions relys on the
(putprop f (invent-pat varlist) 'inpat)
(putprop f t 'postcond)
(putprop f (mk-predbody f varlist) 'body))))
(def mk-params (varlist)
(do ((ct varlist (rest ct))
(l () (cons (intern (gensym)) l)))
((null ct) l)))
(def mk-predbody (f varlist)
(prog (namestring)
(setq namestring (explode f))
(return (cond ((eq (second namestring) 'f)
(eval (list 'defun f 'fexpr '(argl)
(list 'prog '(seplist outpos)
'(setq seplist (split argl))
'(setq outpos (second seplist))
(list 'return
(list 'cond
(list '(is-var outpos)
(list 'list
(list 'cons
'outpos
(list 'eval
(list 'cons
(list 'quote
(cond
((eq (third namestring) '//)
(implode (rest (rest (rest namestring)))))
(t
(implode
(rest (rest
namestring))
))) )
'(first seplist))) )))
(list (list
'equal
'outpos
(list 'eval
(list 'cons
(list 'quote
(cond
((eq (third namestring) '//)
(implode (rest (rest (rest namestring)))))
(t
(implode
(rest (rest
namestring))
))) )
'(first seplist))) )
() )
(list t ''undef) ))))))
((eq (second namestring) 'p)
(eval (list 'defun f 'fexpr '(argl)
(list 'prog '(seplist ans)
'(setq seplist (split argl))
(list 'setq
'ans
(list 'eval
(list 'cons
(list 'quote
(implode
(rest (rest
namestring))
))
'(first seplist))))
'(return
(cond
((is-var (second seplist))
(list (cons (second seplist)
ans)))
((equal ans (second seplist))
() )
(t 'undef)))
))) )
(t (error '(autopred called w/no %p or %f) f))))))
(def split (l) (cond ((null l) (error '(request to split empty list)l))
((null (rest l)) (list () (first l)))
(t ((lambda (h) (cons (cons (first l) (first h))
(rest h)))
(split (rest l))))))
(def invent-pat (varlist)
(do ((ct (rest varlist) (rest ct))
(pat (cons 0 () ) (cons 1 pat)))
((null ct) pat)))